$\forall$${\it rx}$, ${\it ra}$, ${\it rt}$:(Id$\rightarrow$Id), $M$:MsgA.
\\[0ex]Inj(Id; Id; ${\it rx}$) $\Rightarrow$ Inj(Id; Id; ${\it ra}$) $\Rightarrow$ Inj(Id; Id; ${\it rt}$) $\Rightarrow$ ma{-}rename(${\it rx}$;${\it ra}$;${\it rt}$;$M$) $\in$ MsgA